CallGraph cg;       /* pre-computed */
AccessPair[] goals; /* computed on-the-fly */
MethodInfo driver;  /* test driver */

int eval(State jpfState) {
  ThreadInfo[] tis = jpfState.threadInfos();
  for(int i=0; i<tis.length; i++) {
    for(int j=0; j<tis.length && j<i; j++) { 
      MethodInfo ma = tis[i].getCurrentMethod();
      MethodInfo mb = tis[j].getCurrentMethod();
      foreach p:Pair in goals {
        int d = dist(ma, p.mx) * dist(mb, p.my);
        if (d < min) min = d;
      }
    }
  } return min;
}

int dist(MethodInfo mSource, MethodInfo mDest) {
  int result = shortestPath(cg, mSource, mDest);
  if (result == -1) { // mDest not reachable from mSource
    return shortestPathFromDriver(cg, 
                                  driver, mSource, mDest);
  }
}